|
In mathematical logic, the primitive recursive functionals are a generalization of primitive recursive functions into higher type theory. They consist of a collection of functions in all pure finite types. The primitive recursive functionals are important in proof theory and constructive mathematics They are a central part of the Dialectica interpretation of intuitionistic arithmetic developed by Kurt Gödel. In recursion theory, the primitive recursive functionals are an example of higher-type computability, as primitive recursive functions are examples of Turing computability. == Background == Every primitive recursive functional has a type, which tells what kind of inputs it takes and what kind of output it produces. An object of type 0 is simply a natural number; it can also be viewed as a constant function that takes no input and returns an output in the set N of natural numbers. For any two types σ and τ, the type σ→τ represents a function that takes an input of type σ and returns an output of type τ. Thus the function ''f''(''n'') = ''n''+1 is of type 0→0. The types (0→0)→0 and 0→(0→0) are different; by convention, the notation 0→0→0 refers to 0→(0→0). In the jargon of type theory, objects of type 0→0 are called ''functions'' and objects that take inputs of type other than 0 are called ''functionals''. For any two types σ and τ, the type σ×τ represents an ordered pair, the first element of which has type σ and the second element of which has type τ. For example, consider the functional ''A'' takes as inputs a function ''f'' from N to N, and a natural number ''n'', and returns ''f''(''n''). Then ''A'' has type (0 × (0→0))→0. This type can also be written as 0→(0→0)→0, by Currying. The set of (pure) ''finite types'' is the smallest collection of types that includes 0 and is closed under the operations of × and →. A superscript is used to indicate that a variable ''x''τ is assumed to have a certain type τ; the superscript may be omitted when the type is clear from context. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Primitive recursive functional」の詳細全文を読む スポンサード リンク
|